Inference at * 1 
Iof proof for Lemma quotient wf:



1. T : Type
2. E : TT
3. EquivRel(T;x,y.E(x,y))
  (x,y:T//E(x,y))  Type 

latex

 by ((((((Repeat (Unfolds 
``equiv_rel refl sym trans`` 3)) 
CollapseTHEN (Unfold `member` 0)))

CollapseTHEN (PrimEqCD))) 
CollapseTHENM ((Auto_aux (first_nat 1:n) ((first_nat 1:n
C),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C1: .....eq aux..... NILNIL

C1: 3. (a:T. E(a,a)) & (a, b:T. E(a,b)  E(b,a)) & (a, b, c:T. E(a,b)  E(b,c)  E(a,c))
C1: 4. x : T
C1:   E(x,x)
C2: .....eq aux..... NILNIL

C2: 3. (a:T. E(a,a)) & (a, b:T. E(a,b)  E(b,a)) & (a, b, c:T. E(a,b)  E(b,c)  E(a,c))
C2: 4. x : T
C2: 5. y : T
C2: 6. E(x,y)
C2:   E(y,x)
C3: .....eq aux..... NILNIL

C3: 3. (a:T. E(a,a)) & (a, b:T. E(a,b)  E(b,a)) & (a, b, c:T. E(a,b)  E(b,c)  E(a,c))
C3: 4. x : T
C3: 5. y : T
C3: 6. x1 : T
C3: 7. E(x,y)
C3: 8. E(y,x1)
C3:   E(x,x1)
C.

Definitions

t  T, x(s1,s2), , Trans(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), P & Q, EquivRel(T;x,y.E(x;y))